<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>9. Groups and Rings &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="10. Linear algebra" href="C10_Linear_Algebra.html" />
    <link rel="prev" title="8. Hierarchies" href="C08_Hierarchies.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">9. Groups and Rings</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#monoids-and-groups">9.1. Monoids and Groups</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#monoids-and-their-morphisms">9.1.1. Monoids and their morphisms</a></li>
<li class="toctree-l3"><a class="reference internal" href="#groups-and-their-morphisms">9.1.2. Groups and their morphisms</a></li>
<li class="toctree-l3"><a class="reference internal" href="#subgroups">9.1.3. Subgroups</a></li>
<li class="toctree-l3"><a class="reference internal" href="#concrete-groups">9.1.4. Concrete groups</a></li>
<li class="toctree-l3"><a class="reference internal" href="#group-actions">9.1.5. Group actions</a></li>
<li class="toctree-l3"><a class="reference internal" href="#quotient-groups">9.1.6. Quotient groups</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#rings">9.2. Rings</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#rings-their-units-morphisms-and-subrings">9.2.1. Rings, their units, morphisms and subrings</a></li>
<li class="toctree-l3"><a class="reference internal" href="#ideals-and-quotients">9.2.2. Ideals and quotients</a></li>
<li class="toctree-l3"><a class="reference internal" href="#algebras-and-polynomials">9.2.3. Algebras and polynomials</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">9. </span>Groups and Rings</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C09_Groups_and_Rings.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="groups-and-rings">
<span id="groups-and-ring"></span><h1><span class="section-number">9. </span>Groups and Rings<a class="headerlink" href="#groups-and-rings" title="Link to this heading">&#61633;</a></h1>
<p>We saw in <a class="reference internal" href="C02_Basics.html#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a> how to reason about
operations in groups and rings. Later, in <a class="reference internal" href="C07_Structures.html#section-algebraic-structures"><span class="std std-numref">Section 7.2</span></a>, we saw how
to define abstract algebraic structures, such as group structures, as well as concrete instances
such as the ring structure on the Gaussian integers. <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a> explained how
hierarchies of abstract structures are handled in Mathlib.</p>
<p>In this chapter we work with groups and rings in more detail. We won&#8217;t be able to
cover every aspect of the treatment of these topics in Mathlib, especially since Mathlib is constantly growing.
But we will provide entry points to the library and show how the essential concepts are used.
There is some overlap with the discussion of
<a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a>, but here we will focus on how to use Mathlib instead of the design
decisions behind the way the topics are treated.
So making sense of some of the examples may require reviewing the background from
<a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a>.</p>
<section id="monoids-and-groups">
<span id="groups"></span><h2><span class="section-number">9.1. </span>Monoids and Groups<a class="headerlink" href="#monoids-and-groups" title="Link to this heading">&#61633;</a></h2>
<section id="monoids-and-their-morphisms">
<span id="index-1"></span><span id="index-0"></span><h3><span class="section-number">9.1.1. </span>Monoids and their morphisms<a class="headerlink" href="#monoids-and-their-morphisms" title="Link to this heading">&#61633;</a></h3>
<p>Courses in abstract algebra often start with groups and
then progress to rings, fields, and vector spaces. This involves some contortions when discussing
multiplication on rings since the multiplication operation does not come from a group structure
but many of the proofs carry over verbatim from group theory to this new setting.
The most common fix, when doing mathematics with pen and paper,
is to leave those proofs as exercises. A less efficient but safer and
more formalization-friendly way of proceeding is to use monoids. A <em>monoid</em> structure on a type <cite>M</cite>
is an internal composition law that is associative and has a neutral element.
Monoids are used primarily to accommodate both groups and the multiplicative structure of
rings. But there are also a number of natural examples; for instance, the set of natural numbers
equipped with addition forms a monoid.</p>
<p>From a practical point of view, you can mostly ignore monoids when using Mathlib. But you need
to know they exist when you are looking for a lemma by browsing Mathlib files. Otherwise, you
might end up looking for a statement in the group theory files when it is actually in the found
with monoids because it does not require elements to be invertible.</p>
<p>The type of monoid structures on a type <code class="docutils literal notranslate"><span class="pre">M</span></code> is written <code class="docutils literal notranslate"><span class="pre">Monoid</span> <span class="pre">M</span></code>.
The function <code class="docutils literal notranslate"><span class="pre">Monoid</span></code> is a type class so it will almost always appear as an instance implicit
argument (in other words, in square brackets).
By default, <code class="docutils literal notranslate"><span class="pre">Monoid</span></code> uses multiplicative notation for the operation; for additive notation
use <code class="docutils literal notranslate"><span class="pre">AddMonoid</span></code> instead.
The commutative versions of these structures add the prefix <code class="docutils literal notranslate"><span class="pre">Comm</span></code> before <code class="docutils literal notranslate"><span class="pre">Monoid</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">mul_one</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
</pre></div>
</div>
<p>Note that although <code class="docutils literal notranslate"><span class="pre">AddMonoid</span></code> is found in the library,
it is generally confusing to use additive notation with a non-commutative operation.</p>
<p>The type of morphisms between monoids <code class="docutils literal notranslate"><span class="pre">M</span></code> and <code class="docutils literal notranslate"><span class="pre">N</span></code> is called <code class="docutils literal notranslate"><span class="pre">MonoidHom</span> <span class="pre">M</span> <span class="pre">N</span></code> and written
<code class="docutils literal notranslate"><span class="pre">M</span> <span class="pre">&#8594;*</span> <span class="pre">N</span></code>. Lean will automatically see such a morphism as a function from <code class="docutils literal notranslate"><span class="pre">M</span></code> to <code class="docutils literal notranslate"><span class="pre">N</span></code> when
we apply it to elements of <code class="docutils literal notranslate"><span class="pre">M</span></code>. The additive version is called <code class="docutils literal notranslate"><span class="pre">AddMonoidHom</span></code> and written
<code class="docutils literal notranslate"><span class="pre">M</span> <span class="pre">&#8594;+</span> <span class="pre">N</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">N</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">N</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_zero</span>
</pre></div>
</div>
<p>These morphisms are bundled maps, i.e. they package together a map and some of its properties.
Remember that <a class="reference internal" href="C08_Hierarchies.html#section-hierarchies-morphisms"><span class="std std-numref">Section 8.2</span></a> explains bundled maps;
here we simply note the slightly unfortunate consequence that we cannot use ordinary function
composition to compose maps. Instead, we need to use <code class="docutils literal notranslate"><span class="pre">MonoidHom.comp</span></code> and <code class="docutils literal notranslate"><span class="pre">AddMonoidHom.comp</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">N</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">P</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">P</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">g.comp</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
</section>
<section id="groups-and-their-morphisms">
<h3><span class="section-number">9.1.2. </span>Groups and their morphisms<a class="headerlink" href="#groups-and-their-morphisms" title="Link to this heading">&#61633;</a></h3>
<p>We will have much more to say about groups, which are monoids with the extra
property that every element has an inverse.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">mul_inv_cancel</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p id="index-2">Similar to the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic that we saw earlier, there is a <code class="docutils literal notranslate"><span class="pre">group</span></code> tactic that proves
any identity that holds in any group. (Equivalently, it proves the identities that hold in
free groups.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">group</span>
</pre></div>
</div>
<p id="index-3">There is also a tactic for identities in commutative additive groups called <code class="docutils literal notranslate"><span class="pre">abel</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">abel</span>
</pre></div>
</div>
<p>Interestingly, a group
morphism is nothing more than a monoid morphism between groups. So we can copy and paste one of our
earlier examples, replacing <code class="docutils literal notranslate"><span class="pre">Monoid</span></code> with <code class="docutils literal notranslate"><span class="pre">Group</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
</pre></div>
</div>
<p>Of course we do get some new properties, such as this one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_inv</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>You may be worried that constructing group morphisms will require us to do unnecessary work since
the definition of monoid morphism enforces that neutral elements are sent to neutral elements
while this is automatic in the case of group morphisms. In practice the extra work is not hard,
but, to avoid it, there is a function building a group morphism from a function
between groups that is compatible with the composition laws.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MonoidHom.mk&#39;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>There is also a type <code class="docutils literal notranslate"><span class="pre">MulEquiv</span></code> of group (or monoid) isomorphisms denoted by <code class="docutils literal notranslate"><span class="pre">&#8771;*</span></code> (and
<code class="docutils literal notranslate"><span class="pre">AddEquiv</span></code> denoted by <code class="docutils literal notranslate"><span class="pre">&#8771;+</span></code> in additive notation).
The inverse of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">G</span> <span class="pre">&#8771;*</span> <span class="pre">H</span></code> is <code class="docutils literal notranslate"><span class="pre">MulEquiv.symm</span> <span class="pre">f</span> <span class="pre">:</span> <span class="pre">H</span> <span class="pre">&#8771;*</span> <span class="pre">G</span></code>,
composition of <code class="docutils literal notranslate"><span class="pre">f</span></code> and <code class="docutils literal notranslate"><span class="pre">g</span></code> is <code class="docutils literal notranslate"><span class="pre">MulEquiv.trans</span> <span class="pre">f</span> <span class="pre">g</span></code>, and
the identity isomorphism of <code class="docutils literal notranslate"><span class="pre">G</span></code> is <code class="docutils literal notranslate"><span class="pre">M&#768;ulEquiv.refl</span> <span class="pre">G</span></code>.
Using anonymous projector notation, the first two can be written <code class="docutils literal notranslate"><span class="pre">f.symm</span></code> and
<code class="docutils literal notranslate"><span class="pre">f.trans</span> <span class="pre">g</span></code> respectively.
Elements of this type are automatically coerced to morphisms and functions when necessary.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f.trans</span><span class="w"> </span><span class="n">f.symm</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">MulEquiv.refl</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.self_trans_symm</span>
</pre></div>
</div>
<p>One can use <code class="docutils literal notranslate"><span class="pre">MulEquiv.ofBijective</span></code> to build an isomorphism from a bijective morphism.
Doing so makes the inverse function noncomputable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Function.Bijective</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MulEquiv.ofBijective</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
</section>
<section id="subgroups">
<h3><span class="section-number">9.1.3. </span>Subgroups<a class="headerlink" href="#subgroups" title="Link to this heading">&#61633;</a></h3>
<p>Just as group morphisms are bundled, a subgroup of <code class="docutils literal notranslate"><span class="pre">G</span></code> is also a bundled structure consisting of
a set in <code class="docutils literal notranslate"><span class="pre">G</span></code> with the relevant closure properties.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">H.mul_mem</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hy</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">H.inv_mem</span><span class="w"> </span><span class="n">hx</span>
</pre></div>
</div>
<p>In the example above, it is important to understand that <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> is the type of subgroups
of <code class="docutils literal notranslate"><span class="pre">G</span></code>, rather than a predicate <code class="docutils literal notranslate"><span class="pre">IsSubgroup</span> <span class="pre">H</span></code> where <code class="docutils literal notranslate"><span class="pre">H</span></code> is an element of <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">G</span></code>.
<code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> is endowed with a coercion to <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">G</span></code> and a membership predicate on <code class="docutils literal notranslate"><span class="pre">G</span></code>.
See <a class="reference internal" href="C08_Hierarchies.html#section-hierarchies-subobjects"><span class="std std-numref">Section 8.3</span></a> for an explanation of how and why this is done.</p>
<p>Of course, two subgroups are the same if and only if they have the same elements. This fact
is registered for use with the <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic, which can be used to prove two subgroups are
equal in the same way it is used to prove that two sets are equal.</p>
<p>To state and prove, for example, that <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> is an additive subgroup of <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>,
what we really want is to construct a term of type <code class="docutils literal notranslate"><span class="pre">AddSubgroup</span> <span class="pre">&#8474;</span></code> whose projection to
<code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">&#8474;</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>, or, more precisely, the image of <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> in <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">AddSubgroup</span><span class="w"> </span><span class="n">&#8474;</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">carrier</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Set.range</span><span class="w"> </span><span class="o">((</span><span class="bp">&#8593;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8474;</span><span class="o">)</span>
<span class="w">  </span><span class="n">add_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="n">zero_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="mi">0</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="n">neg_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="bp">-</span><span class="n">n</span>
<span class="w">    </span><span class="n">simp</span>
</pre></div>
</div>
<p>Using type classes, Mathlib knows that a subgroup of a group inherits a group structure.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>This example is subtle. The object <code class="docutils literal notranslate"><span class="pre">H</span></code> is not a type, but Lean automatically coerces it to
a type by interpreting it as a subtype of <code class="docutils literal notranslate"><span class="pre">G</span></code>.
So the above example can be restated more explicitly as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>An important benefit of having a type <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> instead of a predicate
<code class="docutils literal notranslate"><span class="pre">IsSubgroup</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">G</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code> is that one can easily endow <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> with additional structure.
Importantly, it has the structure of a complete lattice structure with respect to
inclusion. For instance, instead of having a lemma stating that an intersection of
two subgroups of <code class="docutils literal notranslate"><span class="pre">G</span></code> is again a subgroup, we
have used the lattice operation <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> to construct the intersection. We can then apply arbitrary
lemmas about lattices to the construction.</p>
<p>Let us check that the set underlying the infimum of two subgroups is indeed, by definition,
their intersection.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It may look strange to have a different notation for what amounts to the intersection of the
underlying sets, but the correspondence does not carry over to the supremum operation and set
union, since a union of subgroups is not, in general, a subgroup.
Instead one needs to use the subgroup generated by the union, which is done
using <code class="docutils literal notranslate"><span class="pre">Subgroup.closure</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Subgroup.closure</span><span class="w"> </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Subgroup.sup_eq_closure</span><span class="o">]</span>
</pre></div>
</div>
<p>Another subtlety is that <code class="docutils literal notranslate"><span class="pre">G</span></code> itself does not have type <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code>,
so we need a way to talk about <code class="docutils literal notranslate"><span class="pre">G</span></code> seen as a subgroup of <code class="docutils literal notranslate"><span class="pre">G</span></code>.
This is also provided by the lattice structure: the full subgroup is the top element of
this lattice.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">trivial</span>
</pre></div>
</div>
<p>Similarly the bottom element of this lattice is the subgroup whose only element is the
neutral element.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Subgroup.mem_bot</span>
</pre></div>
</div>
<p>As an exercise in manipulating groups and subgroups, you can define the conjugate of a subgroup
by an element of the ambient group.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">conjugate</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">carrier</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">h</span><span class="o">,</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="o">}</span>
<span class="w">  </span><span class="n">one_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">dsimp</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">inv_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">dsimp</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">mul_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">dsimp</span>
<span class="w">    </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Tying the previous two topics together, one can push forward and pull back subgroups using
group morphisms. The naming convention in Mathlib is to call those operations <code class="docutils literal notranslate"><span class="pre">map</span></code>
and <code class="docutils literal notranslate"><span class="pre">comap</span></code>.
These are not the common mathematical terms, but they have the advantage of being
shorter than &#8220;pushforward&#8221; and &#8220;direct image.&#8221;</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">G&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Subgroup.map</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">G&#39;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Subgroup.comap</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">H&#39;</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.mem_map</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.mem_comap</span>
</pre></div>
</div>
<p>In particular, the preimage of the bottom subgroup under a morphism <code class="docutils literal notranslate"><span class="pre">f</span></code> is a subgroup called
the <em>kernel</em> of <code class="docutils literal notranslate"><span class="pre">f</span></code>, and the range of <code class="docutils literal notranslate"><span class="pre">f</span></code> is also a subgroup.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">MonoidHom.ker</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.mem_ker</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">h</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">MonoidHom.range</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.mem_range</span>
</pre></div>
</div>
<p>As exercises in manipulating group morphisms and subgroups, let us prove some elementary properties.
They are already proved in Mathlib, so do not use <code class="docutils literal notranslate"><span class="pre">exact?</span></code> too quickly if you want to benefit
from these exercises.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">exercises</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Subgroup</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hST</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hST</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">K</span><span class="o">]</span>

<span class="c1">-- Remember you can use the `ext` tactic to prove an equality of subgroups.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">comap</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;.comp</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">comap</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="c1">-- Pushing a subgroup along one homomorphism and then another is equal to</span>
<span class="c1">-- pushing it forward along the composite of the homomorphisms.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">map</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;.comp</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">map</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">(</span><span class="n">S.map</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">end</span><span class="w"> </span><span class="n">exercises</span>
</pre></div>
</div>
<p>Let us finish this introduction to subgroups in Mathlib with two very classical results.
Lagrange theorem states the cardinality of a subgroup of a finite group divides the cardinality of
the group. Sylow&#8217;s first theorem is a famous partial converse to Lagrange&#8217;s theorem.</p>
<p>While this corner of Mathlib is partly set up to allow computation, we can tell
Lean to use nonconstructive logic anyway using the following <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">scoped</span></code> command.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">scoped</span><span class="w"> </span><span class="n">Classical</span>


<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">G&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G&#39;</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">G&#39;.index</span><span class="o">,</span><span class="w"> </span><span class="n">mul_comm</span><span class="w"> </span><span class="n">G&#39;.index</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#9656;</span><span class="w"> </span><span class="n">G&#39;.index_mul_card.symm</span><span class="o">&#10217;</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Subgroup</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Fact</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">hdvd</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Sylow.exists_subgroup_card_pow_prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="n">hdvd</span>
</pre></div>
</div>
<p>The next two exercises derive a corollary of Lagrange&#8217;s lemma. (This is also already in Mathlib,
so do not use <code class="docutils literal notranslate"><span class="pre">exact?</span></code> too quickly.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span><span class="w"> </span><span class="n">eq_bot_iff_card</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">H</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">suffices</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">simpa</span><span class="w"> </span><span class="o">[</span><span class="n">eq_bot_iff_forall</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.card_eq_one_iff_exists</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="k">#check</span><span class="w"> </span><span class="n">card_dvd_of_le</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">inf_bot_of_coprime</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="bp">.</span><span class="n">Coprime</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="concrete-groups">
<h3><span class="section-number">9.1.4. </span>Concrete groups<a class="headerlink" href="#concrete-groups" title="Link to this heading">&#61633;</a></h3>
<p>One can also manipulate concrete groups in Mathlib, although this is typically more complicated
than working with the abstract theory.
For instance, given any type <code class="docutils literal notranslate"><span class="pre">X</span></code>, the group of permutations of <code class="docutils literal notranslate"><span class="pre">X</span></code> is <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">X</span></code>.
In particular the symmetric group <span class="math notranslate nohighlight">\(\mathfrak{S}_n\)</span> is <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">(Fin</span> <span class="pre">n)</span></code>.
One can state abstract results about this group, for instance saying that <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">X</span></code> is
generated by cycles if <code class="docutils literal notranslate"><span class="pre">X</span></code> is finite.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Equiv</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup.closure</span><span class="w"> </span><span class="o">{</span><span class="n">&#963;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">Perm.IsCycle</span><span class="w"> </span><span class="n">&#963;</span><span class="o">}</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Perm.closure_isCycle</span>
</pre></div>
</div>
<p>One can be fully concrete and compute actual products of cycles. Below we use the <code class="docutils literal notranslate"><span class="pre">#simp</span></code> command,
which calls the <code class="docutils literal notranslate"><span class="pre">simp</span></code> tactic on a given expression. The notation <code class="docutils literal notranslate"><span class="pre">c[]</span></code> is used to define a
cyclic permutation. In the example, the result is a permutation of <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>. One could use a type
ascription such as <code class="docutils literal notranslate"><span class="pre">(1</span> <span class="pre">:</span> <span class="pre">Fin</span> <span class="pre">5)</span></code> on the first number appearing to make it a computation in
<code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">(Fin</span> <span class="pre">5)</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">#</span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">]</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span>
</pre></div>
</div>
<p>Another way to work with concrete groups is to use free groups and group presentations.
The free group on a type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is <code class="docutils literal notranslate"><span class="pre">FreeGroup</span> <span class="pre">&#945;</span></code> and the inclusion map is
<code class="docutils literal notranslate"><span class="pre">FreeGroup.of</span> <span class="pre">:</span> <span class="pre">&#945;</span> <span class="pre">&#8594;</span> <span class="pre">FreeGroup</span> <span class="pre">&#945;</span></code>. For instance let us define a type <code class="docutils literal notranslate"><span class="pre">S</span></code> with three elements denoted
by <code class="docutils literal notranslate"><span class="pre">a</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code> and <code class="docutils literal notranslate"><span class="pre">c</span></code>, and the element <code class="docutils literal notranslate"><span class="pre">ab&#8315;&#185;</span></code> of the corresponding free group.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">FreeGroup</span>

<span class="kd">inductive</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">c</span>

<span class="kn">open</span><span class="w"> </span><span class="n">S</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myElement</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">FreeGroup</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">&#8315;&#185;</span>
</pre></div>
</div>
<p>Note that we gave the expected type of the definition so that Lean knows that <code class="docutils literal notranslate"><span class="pre">.of</span></code> means
<code class="docutils literal notranslate"><span class="pre">FreeGroup.of</span></code>.</p>
<p>The universal property of free groups is embodied as the equivalence <code class="docutils literal notranslate"><span class="pre">FreeGroup.lift</span></code>.
For example, let us define the group morphism from <code class="docutils literal notranslate"><span class="pre">FreeGroup</span> <span class="pre">S</span></code> to <code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">(Fin</span> <span class="pre">5)</span></code> that
sends <code class="docutils literal notranslate"><span class="pre">a</span></code> to <code class="docutils literal notranslate"><span class="pre">c[1,</span> <span class="pre">2,</span> <span class="pre">3]</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code> to <code class="docutils literal notranslate"><span class="pre">c[2,</span> <span class="pre">3,</span> <span class="pre">1]</span></code>, and <code class="docutils literal notranslate"><span class="pre">c</span></code> to <code class="docutils literal notranslate"><span class="pre">c[2,</span> <span class="pre">3]</span></code>,</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myMorphism</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">FreeGroup</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">FreeGroup.lift</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="bp">.</span><span class="n">a</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span>
<span class="w">                     </span><span class="bp">|</span><span class="w"> </span><span class="bp">.</span><span class="n">b</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span>
<span class="w">                     </span><span class="bp">|</span><span class="w"> </span><span class="bp">.</span><span class="n">c</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span>
</pre></div>
</div>
<p>As a last concrete example, let us see how to define a group generated by a single element whose
cube is one (so that group will be isomorphic to <span class="math notranslate nohighlight">\(\mathbb{Z}/3\)</span>) and build a morphism
from that group to <code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">(Fin</span> <span class="pre">5)</span></code>.</p>
<p>As a type with exactly one element, we will use <code class="docutils literal notranslate"><span class="pre">Unit</span></code> whose
only element is denoted by <code class="docutils literal notranslate"><span class="pre">()</span></code>. The function <code class="docutils literal notranslate"><span class="pre">PresentedGroup</span></code> takes a set of relations,
i.e. a set of elements of some free group, and returns a group that is this free group quotiented
by a normal subgroup generated by relations. (We will see how to handle more general quotients
in <a class="reference internal" href="#quotient-groups"><span class="std std-numref">Section 9.1.6</span></a>.) Since we somehow hide this behind a definition, we use <code class="docutils literal notranslate"><span class="pre">deriving</span> <span class="pre">Group</span></code> to force creation
of a group instance on <code class="docutils literal notranslate"><span class="pre">myGroup</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myGroup</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">PresentedGroup</span><span class="w"> </span><span class="o">{</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="o">()</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">3</span><span class="o">}</span><span class="w"> </span><span class="n">deriving</span><span class="w"> </span><span class="n">Group</span>
</pre></div>
</div>
<p>The universal property of presented groups ensures that morphisms out of this group can be built
from functions that send the relations to the neutral element of the target group.
So we need such a function and a proof that the condition holds. Then we can feed this proof
to <code class="docutils literal notranslate"><span class="pre">PresentedGroup.toGroup</span></code> to get the desired group morphism.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myMap</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Unit</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span>
<span class="bp">|</span><span class="w"> </span><span class="o">()</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">compat_myMap</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">({</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="o">()</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">3</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="o">(</span><span class="n">FreeGroup</span><span class="w"> </span><span class="n">Unit</span><span class="o">)),</span><span class="w"> </span><span class="n">FreeGroup.lift</span><span class="w"> </span><span class="n">myMap</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">simp</span>
<span class="w">  </span><span class="n">decide</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myNewMorphism</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">myGroup</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">PresentedGroup.toGroup</span><span class="w"> </span><span class="n">compat_myMap</span>

<span class="kd">end</span><span class="w"> </span><span class="n">FreeGroup</span>
</pre></div>
</div>
</section>
<section id="group-actions">
<h3><span class="section-number">9.1.5. </span>Group actions<a class="headerlink" href="#group-actions" title="Link to this heading">&#61633;</a></h3>
<p>One important way that group theory interacts with the rest of mathematics is through
the use of group actions.
An action of a group <code class="docutils literal notranslate"><span class="pre">G</span></code> on some type <code class="docutils literal notranslate"><span class="pre">X</span></code> is nothing more than a morphism from <code class="docutils literal notranslate"><span class="pre">G</span></code> to
<code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">X</span></code>. So in a sense group actions are already covered by the previous discussion.
But we don&#8217;t want to carry this morphism around; instead, we want it to be inferred automatically
by Lean as much as possible. So we have a type class for this, which is <code class="docutils literal notranslate"><span class="pre">MulAction</span> <span class="pre">G</span> <span class="pre">X</span></code>.
The downside of this setup is that having multiple actions of the same group on the same type
requires some contortions, such as defining type synonyms, each of which carries different
type class instances.</p>
<p>This allows us in particular to use <code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">&#8226;</span> <span class="pre">x</span></code> to denote the action of a group element <code class="docutils literal notranslate"><span class="pre">g</span></code> on
a point <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span><span class="w"> </span><span class="n">GroupActions</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">(</span><span class="n">g&#39;</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">mul_smul</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
</pre></div>
</div>
<p>There is also a version for additive group called <code class="docutils literal notranslate"><span class="pre">AddAction</span></code>, where the action is denoted by
<code class="docutils literal notranslate"><span class="pre">+&#7525;</span></code>. This is used for instance in the definition of affine spaces.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddGroup</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">g</span><span class="w"> </span><span class="bp">+&#7525;</span><span class="w"> </span><span class="o">(</span><span class="n">g&#39;</span><span class="w"> </span><span class="bp">+&#7525;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">g&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">+&#7525;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">add_vadd</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
</pre></div>
</div>
<p>The underlying group morphism is called <code class="docutils literal notranslate"><span class="pre">MulAction.toPermHom</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">MulAction</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">toPermHom</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span>
</pre></div>
</div>
<p>As an illustration let us see how to define the Cayley isomorphism embedding of any group <code class="docutils literal notranslate"><span class="pre">G</span></code> into
a permutation group, namely <code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">G</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">CayleyIsoMorphism</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="o">(</span><span class="n">toPermHom</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="bp">.</span><span class="n">range</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Equiv.Perm.subgroupOfMulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">G</span>
</pre></div>
</div>
<p>Note that nothing before the above definition required having a group rather than a monoid (or any
type endowed with a multiplication operation really).</p>
<p>The group condition really enters the picture when we will want to partition <code class="docutils literal notranslate"><span class="pre">X</span></code> into orbits.
The corresponding equivalence relation on <code class="docutils literal notranslate"><span class="pre">X</span></code> is called <code class="docutils literal notranslate"><span class="pre">MulAction.orbitRel</span></code>.
It is not declared as a global instance.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Setoid</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">orbitRel</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span>
</pre></div>
</div>
<p>Using this we can state that <code class="docutils literal notranslate"><span class="pre">X</span></code> is partitioned into orbits under the action of <code class="docutils literal notranslate"><span class="pre">G</span></code>.
More precisely, we get a bijection between <code class="docutils literal notranslate"><span class="pre">X</span></code> and the dependent product
<code class="docutils literal notranslate"><span class="pre">(&#969;</span> <span class="pre">:</span> <span class="pre">orbitRel.Quotient</span> <span class="pre">G</span> <span class="pre">X)</span> <span class="pre">&#215;</span> <span class="pre">(orbit</span> <span class="pre">G</span> <span class="pre">(Quotient.out'</span> <span class="pre">&#969;))</span></code>
where <code class="docutils literal notranslate"><span class="pre">Quotient.out'</span> <span class="pre">&#969;</span></code> simply chooses an element that projects to <code class="docutils literal notranslate"><span class="pre">&#969;</span></code>.
Recall that elements of this dependent product are pairs <code class="docutils literal notranslate"><span class="pre">&#10216;&#969;,</span> <span class="pre">x&#10217;</span></code> where the type
<code class="docutils literal notranslate"><span class="pre">orbit</span> <span class="pre">G</span> <span class="pre">(Quotient.out'</span> <span class="pre">&#969;)</span></code> of <code class="docutils literal notranslate"><span class="pre">x</span></code> depends on <code class="docutils literal notranslate"><span class="pre">&#969;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">X</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="o">(</span><span class="n">&#969;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">orbitRel.Quotient</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="o">(</span><span class="n">orbit</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">(</span><span class="n">Quotient.out</span><span class="w"> </span><span class="n">&#969;</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MulAction.selfEquivSigmaOrbits</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span>
</pre></div>
</div>
<p>In particular, when X is finite, this can be combined with <code class="docutils literal notranslate"><span class="pre">Fintype.card_congr</span></code> and
<code class="docutils literal notranslate"><span class="pre">Fintype.card_sigma</span></code> to deduce that the cardinality of <code class="docutils literal notranslate"><span class="pre">X</span></code> is the sum of the cardinalities
of the orbits.
Furthermore, the orbits are in bijection with the quotient of <code class="docutils literal notranslate"><span class="pre">G</span></code> under the action of the
stabilizers by left translation.
This action of a subgroup by left-translation is used to define quotients of a group by a
subgroup with notation <cite>/</cite> so we can use the following concise statement.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">orbit</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">stabilizer</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MulAction.orbitEquivQuotientStabilizer</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>An important special case of combining the above two results is when <code class="docutils literal notranslate"><span class="pre">X</span></code> is a group <code class="docutils literal notranslate"><span class="pre">G</span></code>
equipped with the action of a subgroup <code class="docutils literal notranslate"><span class="pre">H</span></code> by translation.
In this case all stabilizers are trivial so every orbit is in bijection with <code class="docutils literal notranslate"><span class="pre">H</span></code> and we get:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">groupEquivQuotientProdSubgroup</span>
</pre></div>
</div>
<p>This is the conceptual variant of the version of Lagrange theorem that we saw above.
Note this version makes no finiteness assumption.</p>
<p>As an exercise for this section, let us build the action of a group on its subgroup by
conjugation, using our definition of <code class="docutils literal notranslate"><span class="pre">conjugate</span></code> from a previous exercise.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">conjugate_one</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">conjugate</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">(</span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">smul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">conjugate</span>
<span class="w">  </span><span class="n">one_smul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">mul_smul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>

<span class="kd">end</span><span class="w"> </span><span class="n">GroupActions</span>
</pre></div>
</div>
</section>
<section id="quotient-groups">
<span id="id1"></span><h3><span class="section-number">9.1.6. </span>Quotient groups<a class="headerlink" href="#quotient-groups" title="Link to this heading">&#61633;</a></h3>
<p>In the above discussion of subgroups acting on groups, we saw the quotient <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">H</span></code> appear.
In general this is only a type. It can be endowed with a group structure such that the quotient
map is a group morphism if and only if <code class="docutils literal notranslate"><span class="pre">H</span></code> is a normal subgroup (and this group structure is
then unique).</p>
<p>The normality assumption is a type class <code class="docutils literal notranslate"><span class="pre">Subgroup.Normal</span></code> so that type class inference can use it
to derive the group structure on the quotient.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span><span class="w"> </span><span class="n">QuotientGroup</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">H.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">H.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.mk&#39;</span><span class="w"> </span><span class="n">H</span>
</pre></div>
</div>
<p>The universal property of quotient groups is accessed through <code class="docutils literal notranslate"><span class="pre">QuotientGroup.lift</span></code>:
a group morphism <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> descends to <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code> as soon as its kernel contains <code class="docutils literal notranslate"><span class="pre">N</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">N.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>
<span class="w">    </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">MonoidHom.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.lift</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The fact that the target group is called <code class="docutils literal notranslate"><span class="pre">M</span></code> is the above snippet is a clue that having a
monoid structure on <code class="docutils literal notranslate"><span class="pre">M</span></code> would be enough.</p>
<p>An important special case is when <code class="docutils literal notranslate"><span class="pre">N</span> <span class="pre">=</span> <span class="pre">ker</span> <span class="pre">&#966;</span></code>. In that case the descended morphism is
injective and we get a group isomorphism onto its image. This result is often called
the first isomorphism theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">MonoidHom.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">MonoidHom.range</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.quotientKerEquivRange</span><span class="w"> </span><span class="n">&#966;</span>
</pre></div>
</div>
<p>Applying the universal property to a composition of a morphism <code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">:</span> <span class="pre">G</span> <span class="pre">&#8594;*</span> <span class="pre">G'</span></code>
with a quotient group projection <code class="docutils literal notranslate"><span class="pre">Quotient.mk'</span> <span class="pre">N'</span></code>,
we can also aim for a morphism from <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code> to <code class="docutils literal notranslate"><span class="pre">G'</span> <span class="pre">&#10744;</span> <span class="pre">N'</span></code>.
The condition required on <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> is usually formulated by saying &#8220;<code class="docutils literal notranslate"><span class="pre">&#966;</span></code> should send <code class="docutils literal notranslate"><span class="pre">N</span></code> inside
<code class="docutils literal notranslate"><span class="pre">N'</span></code>.&#8221; But this is equivalent to asking that <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> should pull <code class="docutils literal notranslate"><span class="pre">N'</span></code> back over
<code class="docutils literal notranslate"><span class="pre">N</span></code>, and the latter condition is nicer to work with since the definition of pullback does not
involve an existential quantifier.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">]</span>
<span class="w">    </span><span class="o">{</span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">N.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">N&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">N&#39;.Normal</span><span class="o">]</span>
<span class="w">    </span><span class="o">{</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Subgroup.comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">N&#39;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">G&#39;</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N&#39;</span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.map</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="n">N&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>One subtle point to keep in mind is that the type <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code> really depends on <code class="docutils literal notranslate"><span class="pre">N</span></code>
(up to definitional equality), so having a proof that two normal subgroups <code class="docutils literal notranslate"><span class="pre">N</span></code> and <code class="docutils literal notranslate"><span class="pre">M</span></code> are equal
is not enough to make the corresponding quotients equal. However the universal properties does give
an isomorphism in this case.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">M.Normal</span><span class="o">]</span>
<span class="w">    </span><span class="o">[</span><span class="n">N.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">QuotientGroup.quotientMulEquivOfEq</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>As a final series of exercises for this section, we will prove that if <code class="docutils literal notranslate"><span class="pre">H</span></code> and <code class="docutils literal notranslate"><span class="pre">K</span></code> are disjoint
normal subgroups of a finite group <code class="docutils literal notranslate"><span class="pre">G</span></code> such that the product of their cardinalities is equal to
the cardinality of <code class="docutils literal notranslate"><span class="pre">G</span></code>
then <code class="docutils literal notranslate"><span class="pre">G</span></code> is isomorphic to <code class="docutils literal notranslate"><span class="pre">H</span> <span class="pre">&#215;</span> <span class="pre">K</span></code>. Recall that disjoint in this context means <code class="docutils literal notranslate"><span class="pre">H</span> <span class="pre">&#8851;</span> <span class="pre">K</span> <span class="pre">=</span> <span class="pre">&#8869;</span></code>.</p>
<p>We start with playing a bit with Lagrange&#8217;s lemma, without assuming the subgroups are normal
or disjoint.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span>

<span class="kn">open</span><span class="w"> </span><span class="n">MonoidHom</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Nat.card_pos</span><span class="w"> </span><span class="c1">-- The nonempty argument will be automatically inferred for subgroups</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.index_eq_card</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.index_mul_card</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.eq_of_mul_eq_mul_right</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">aux_card_eq</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Nat.card</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>From now on, we assume that our subgroups are normal and disjoint, and we assume the cardinality
condition. Now we construct the first building block of the desired isomorphism.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">H.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">K.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Disjoint</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>
<span class="w">  </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Nat.bijective_iff_injective_and_card</span>
<span class="k">#check</span><span class="w"> </span><span class="n">ker_eq_bot_iff</span>
<span class="k">#check</span><span class="w"> </span><span class="n">restrict</span>
<span class="k">#check</span><span class="w"> </span><span class="n">ker_restrict</span>

<span class="kd">def</span><span class="w"> </span><span class="n">iso&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Now we can define our second building block.
We will need <code class="docutils literal notranslate"><span class="pre">MonoidHom.prod</span></code>, which builds a morphism from <code class="docutils literal notranslate"><span class="pre">G&#8320;</span></code> to <code class="docutils literal notranslate"><span class="pre">G&#8321;</span> <span class="pre">&#215;</span> <span class="pre">G&#8322;</span></code> out of
morphisms from <code class="docutils literal notranslate"><span class="pre">G&#8320;</span></code> to <code class="docutils literal notranslate"><span class="pre">G&#8321;</span></code> and <code class="docutils literal notranslate"><span class="pre">G&#8322;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">iso&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We are ready to put all pieces together.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">MulEquiv.prodCongr</span>

<span class="kd">def</span><span class="w"> </span><span class="n">finalIso</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
</section>
<section id="rings">
<span id="id2"></span><h2><span class="section-number">9.2. </span>Rings<a class="headerlink" href="#rings" title="Link to this heading">&#61633;</a></h2>
<section id="rings-their-units-morphisms-and-subrings">
<span id="index-4"></span><h3><span class="section-number">9.2.1. </span>Rings, their units, morphisms and subrings<a class="headerlink" href="#rings-their-units-morphisms-and-subrings" title="Link to this heading">&#61633;</a></h3>
<p>The type of ring structures on a type <code class="docutils literal notranslate"><span class="pre">R</span></code> is <code class="docutils literal notranslate"><span class="pre">Ring</span> <span class="pre">R</span></code>. The variant where multiplication is
assumed to be commutative is <code class="docutils literal notranslate"><span class="pre">CommRing</span> <span class="pre">R</span></code>. We have already seen that the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic will
prove any equality that follows from the axioms of a commutative ring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
</pre></div>
</div>
<p>More exotic variants do not require that the addition on <code class="docutils literal notranslate"><span class="pre">R</span></code> forms a group but only an additive
monoid. The corresponding type classes are <code class="docutils literal notranslate"><span class="pre">Semiring</span> <span class="pre">R</span></code> and <code class="docutils literal notranslate"><span class="pre">CommSemiring</span> <span class="pre">R</span></code>.
The type of natural numbers is an important instance of <code class="docutils literal notranslate"><span class="pre">CommSemiring</span> <span class="pre">R</span></code>, as is any type
of functions taking values in the natural numbers.
Another important example is the type of ideals in a ring, which will be discussed below.
The name of the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic is doubly misleading, since it assumes commutativity but works
in semirings as well. In other words, it applies to any <code class="docutils literal notranslate"><span class="pre">CommSemiring</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
</pre></div>
</div>
<p>There are also versions of the ring and semiring classes that do not assume the existence of a
multiplicative unit or
the associativity of multiplication. We will not discuss those here.</p>
<p>Some concepts that are traditionally taught in an introduction to ring theory are actually about
the underlying multiplicative monoid.
A prominent example is the definition of the units of a ring. Every (multiplicative) monoid <code class="docutils literal notranslate"><span class="pre">M</span></code>
has a predicate <code class="docutils literal notranslate"><span class="pre">IsUnit</span> <span class="pre">:</span> <span class="pre">M</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code> asserting existence of a two-sided inverse, a
type <code class="docutils literal notranslate"><span class="pre">Units</span> <span class="pre">M</span></code> of units with notation <code class="docutils literal notranslate"><span class="pre">M&#739;</span></code>, and a coercion to <code class="docutils literal notranslate"><span class="pre">M</span></code>.
The type <code class="docutils literal notranslate"><span class="pre">Units</span> <span class="pre">M</span></code> bundles an invertible element with its inverse as well as properties than ensure
that each is indeed the inverse of the other.
This implementation detail is relevant mainly when defining computable functions. In most
situations one can use <code class="docutils literal notranslate"><span class="pre">IsUnit.unit</span> <span class="pre">{x</span> <span class="pre">:</span> <span class="pre">M}</span> <span class="pre">:</span> <span class="pre">IsUnit</span> <span class="pre">x</span> <span class="pre">&#8594;</span> <span class="pre">M&#739;</span></code> to build a unit.
In the commutative case, one also has <code class="docutils literal notranslate"><span class="pre">Units.mkOfMulEqOne</span> <span class="pre">(x</span> <span class="pre">y</span> <span class="pre">:</span> <span class="pre">M)</span> <span class="pre">:</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">1</span> <span class="pre">&#8594;</span> <span class="pre">M&#739;</span></code>
which builds <code class="docutils literal notranslate"><span class="pre">x</span></code> seen as unit.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="bp">&#739;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.units_eq_one_or</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="bp">&#739;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Units.mul_inv</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="n">M</span><span class="bp">&#739;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>The type of ring morphisms between two (semi)-rings <code class="docutils literal notranslate"><span class="pre">R</span></code> and <code class="docutils literal notranslate"><span class="pre">S</span></code> is <code class="docutils literal notranslate"><span class="pre">RingHom</span> <span class="pre">R</span> <span class="pre">S</span></code>,
with notation <code class="docutils literal notranslate"><span class="pre">R</span> <span class="pre">&#8594;+*</span> <span class="pre">S</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">f.map_add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="bp">&#739;</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">S</span><span class="bp">&#739;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Units.map</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
<p>The isomorphism variant is <code class="docutils literal notranslate"><span class="pre">RingEquiv</span></code>, with notation <code class="docutils literal notranslate"><span class="pre">&#8771;+*</span></code>.</p>
<p>As with submonoids and subgroups, there is a <code class="docutils literal notranslate"><span class="pre">Subring</span> <span class="pre">R</span></code> type for subrings of a ring <code class="docutils literal notranslate"><span class="pre">R</span></code>,
but this type is a lot less useful than the type of subgroups since one cannot quotient a ring by
a subring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subring</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ring</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>Also notice that <code class="docutils literal notranslate"><span class="pre">RingHom.range</span></code> produces a subring.</p>
</section>
<section id="ideals-and-quotients">
<h3><span class="section-number">9.2.2. </span>Ideals and quotients<a class="headerlink" href="#ideals-and-quotients" title="Link to this heading">&#61633;</a></h3>
<p>For historical reasons, Mathlib only has a theory of ideals for commutative rings.
(The ring library was originally developed to make quick progress toward the foundations of modern
algebraic geometry.) So in this section we will work with commutative (semi)rings.
Ideals of <code class="docutils literal notranslate"><span class="pre">R</span></code> are defined as submodules of <code class="docutils literal notranslate"><span class="pre">R</span></code> seen as <code class="docutils literal notranslate"><span class="pre">R</span></code>-modules. Modules will
be covered later in a chapter on linear algebra, but this implementation detail can mostly be
safely ignored since most (but not all) relevant lemmas are restated in the special context of
ideals. But anonymous projection notation won&#8217;t always work as expected. For instance,
one cannot replace <code class="docutils literal notranslate"><span class="pre">Ideal.Quotient.mk</span> <span class="pre">I</span></code> by <code class="docutils literal notranslate"><span class="pre">I.Quotient.mk</span></code> in the snippet below because there
are two <code class="docutils literal notranslate"><span class="pre">.</span></code>s and so it will parse as <code class="docutils literal notranslate"><span class="pre">(Ideal.Quotient</span> <span class="pre">I).mk</span></code>; but <code class="docutils literal notranslate"><span class="pre">Ideal.Quotient</span></code> by itself
doesn&#8217;t exist.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.Quotient.mk</span><span class="w"> </span><span class="n">I</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Ideal.Quotient.mk</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.Quotient.eq_zero_iff_mem</span>
</pre></div>
</div>
<p>The universal property of quotient rings is <code class="docutils literal notranslate"><span class="pre">Ideal.Quotient.lift</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">RingHom.ker</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.Quotient.lift</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">H</span>
</pre></div>
</div>
<p>In particular it leads to the first isomorphism theorem for rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">S</span><span class="o">](</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">RingHom.ker</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="n">f.range</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">RingHom.quotientKerEquivRange</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
<p>Ideals form a complete lattice structure with the inclusion relation, as well as a semiring
structure. These two structures interact nicely.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">I</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">J</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Submodule.mem_sup</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Ideal.mul_le_left</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Ideal.mul_le_right</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Ideal.mul_le_inf</span>
</pre></div>
</div>
<p>One can use ring morphisms to push ideals forward and pull them back using <code class="docutils literal notranslate"><span class="pre">Ideal.map</span></code> and
<code class="docutils literal notranslate"><span class="pre">Ideal.comap</span></code>, respectively. As usual,
the latter is more convenient to use since it does not involve an existential quantifier.
This explains why it is used to state the condition that allows us to build morphisms between
quotient rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Ideal.comap</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">J</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.quotientMap</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">H</span>
</pre></div>
</div>
<p>One subtle point is that the type <code class="docutils literal notranslate"><span class="pre">R</span> <span class="pre">&#10744;</span> <span class="pre">I</span></code> really depends on <code class="docutils literal notranslate"><span class="pre">I</span></code>
(up to definitional equality), so having a proof that two ideals <code class="docutils literal notranslate"><span class="pre">I</span></code> and <code class="docutils literal notranslate"><span class="pre">J</span></code> are equal is not
enough to make the corresponding quotients equal. However, the universal properties do provide
an isomorphism in this case.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">J</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.quotEquivOfEq</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We can now present the Chinese remainder isomorphism as an example. Pay attention to the difference
between the indexed infimum symbol <code class="docutils literal notranslate"><span class="pre">&#10757;</span></code> and the big product of types symbol <code class="docutils literal notranslate"><span class="pre">&#928;</span></code>. Depending on
your font, those can be pretty hard to distinguish.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.quotientInfRingEquivPiQuotient</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hf</span>
</pre></div>
</div>
<p>The elementary version of the Chinese remainder theorem, a statement about <code class="docutils literal notranslate"><span class="pre">ZMod</span></code>, can be easily
deduced from the previous one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">BigOperators</span><span class="w"> </span><span class="n">PiNotation</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">coprime</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="bp">.</span><span class="n">Coprime</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">ZMod</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">ZMod</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">ZMod.prodEquivPi</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">coprime</span>
</pre></div>
</div>
<p>As a series of exercises, we will reprove the Chinese remainder theorem in the general case.</p>
<p>We first need to define the map appearing in the theorem, as a ring morphism, using the
universal property of quotient rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
<span class="kn">open</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">Quotient</span><span class="w"> </span><span class="n">Function</span>

<span class="k">#check</span><span class="w"> </span><span class="k">Pi</span><span class="bp">.</span><span class="n">ringHom</span>
<span class="k">#check</span><span class="w"> </span><span class="n">ker_Pi_Quotient_mk</span>

<span class="sd">/-- The homomorphism from ``R &#10744; &#10757; i, I i`` to ``&#928; i, R &#10744; I i`` featured in the Chinese</span>
<span class="sd">  Remainder Theorem. -/</span>
<span class="kd">def</span><span class="w"> </span><span class="n">chineseMap</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Make sure the following next two lemmas can be proven by <code class="docutils literal notranslate"><span class="pre">rfl</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="n">Quotient.mk</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">Ideal.Quotient.mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_mk&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="n">mk</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>The next lemma proves the easy half of the Chinese remainder theorem, without any assumption on
the family of ideals. The proof is less than one line long.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">injective_lift_iff</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_inj</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Injective</span><span class="w"> </span><span class="o">(</span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We are now ready for the heart of the theorem, which will show the surjectivity
of our <code class="docutils literal notranslate"><span class="pre">chineseMap</span></code>. First we need to know the different ways one can express the coprimality
(also called co-maximality assumption). Only the first two will be needed below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">IsCoprime</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_add</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_exists</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_sup_eq</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_codisjoint</span>
</pre></div>
</div>
<p>We take the opportunity to use induction on <code class="docutils literal notranslate"><span class="pre">Finset</span></code>. Relevant lemmas on <code class="docutils literal notranslate"><span class="pre">Finset</span></code> are given
below.
Remember that the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic works for semirings and that the ideals of a ring form a semiring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Finset.mem_insert_of_mem</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Finset.mem_insert_self</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">isCoprime_Inf</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#953;</span><span class="o">}</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="n">J</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">classical</span>
<span class="w">  </span><span class="n">simp_rw</span><span class="w"> </span><span class="o">[</span><span class="n">isCoprime_iff_add</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="bp">*</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Finset.induction</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">empty</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="n">simp</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="bp">@</span><span class="n">insert</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">hs</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Finset.iInf_insert</span><span class="o">,</span><span class="w"> </span><span class="n">inf_comm</span><span class="o">,</span><span class="w"> </span><span class="n">one_eq_top</span><span class="o">,</span><span class="w"> </span><span class="n">eq_top_iff</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">one_eq_top</span><span class="o">]</span>
<span class="w">      </span><span class="n">set</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">j</span>
<span class="w">      </span><span class="k">calc</span>
<span class="w">        </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w">                  </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">        </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w">      </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">        </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">i</span><span class="w">  </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">        </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">i</span><span class="w">            </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We can now prove surjectivity of the map appearing in the Chinese remainder theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_surj</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span>
<span class="w">    </span><span class="o">(</span><span class="n">hI</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Surjective</span><span class="w"> </span><span class="o">(</span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">classical</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">g</span>
<span class="w">  </span><span class="n">choose</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">Ideal.Quotient.mk_surjective</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="o">)</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">key</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">i</span>
<span class="w">    </span><span class="k">have</span><span class="w"> </span><span class="n">hI&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">({</span><span class="n">i</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="bp">&#7580;</span><span class="o">,</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">choose</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">he</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">key</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">i</span><span class="o">)</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Now all the pieces come together in the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">def</span><span class="w"> </span><span class="n">chineseIso</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">Equiv.ofBijective</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">chineseMap_inj</span><span class="w"> </span><span class="n">f</span><span class="o">,</span><span class="w"> </span><span class="n">chineseMap_surj</span><span class="w"> </span><span class="n">hf</span><span class="o">&#10217;,</span>
<span class="w">    </span><span class="n">chineseMap</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">}</span>
</pre></div>
</div>
</section>
<section id="algebras-and-polynomials">
<h3><span class="section-number">9.2.3. </span>Algebras and polynomials<a class="headerlink" href="#algebras-and-polynomials" title="Link to this heading">&#61633;</a></h3>
<p>Given a commutative (semi)ring <code class="docutils literal notranslate"><span class="pre">R</span></code>, an <em>algebra over</em> <code class="docutils literal notranslate"><span class="pre">R</span></code> is a semiring <code class="docutils literal notranslate"><span class="pre">A</span></code> equipped
with a ring morphism whose image commutes with every element of <code class="docutils literal notranslate"><span class="pre">A</span></code>. This is encoded as
a type class <code class="docutils literal notranslate"><span class="pre">Algebra</span> <span class="pre">R</span> <span class="pre">A</span></code>.
The morphism from <code class="docutils literal notranslate"><span class="pre">R</span></code> to <code class="docutils literal notranslate"><span class="pre">A</span></code> is called the structure map and is denoted
<code class="docutils literal notranslate"><span class="pre">algebraMap</span> <span class="pre">R</span> <span class="pre">A</span> <span class="pre">:</span> <span class="pre">R</span> <span class="pre">&#8594;+*</span> <span class="pre">A</span></code> in Lean.
Multiplication of <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">:</span> <span class="pre">A</span></code> by <code class="docutils literal notranslate"><span class="pre">algebraMap</span> <span class="pre">R</span> <span class="pre">A</span> <span class="pre">r</span></code> for some <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">:</span> <span class="pre">R</span></code> is called the scalar
multiplication of <code class="docutils literal notranslate"><span class="pre">a</span></code> by <code class="docutils literal notranslate"><span class="pre">r</span></code> and denoted by <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">&#8226;</span> <span class="pre">a</span></code>.
Note that this notion of algebra is sometimes called an <em>associative unital algebra</em> to emphasize the
existence of more general notions of algebra.</p>
<p>The fact that <code class="docutils literal notranslate"><span class="pre">algebraMap</span> <span class="pre">R</span> <span class="pre">A</span></code> is ring morphism packages together a lot of properties of scalar
multiplication, such as the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Algebra</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">r&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">add_smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="n">a</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Algebra</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">r&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mul_smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="n">a</span>
</pre></div>
</div>
<p>The morphisms between two <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebras <code class="docutils literal notranslate"><span class="pre">A</span></code> and <code class="docutils literal notranslate"><span class="pre">B</span></code> are ring morphisms
which commute with scalar multiplication by elements of <code class="docutils literal notranslate"><span class="pre">R</span></code>. They are bundled morphisms
with type <code class="docutils literal notranslate"><span class="pre">AlgHom</span> <span class="pre">R</span> <span class="pre">A</span> <span class="pre">B</span></code>, which is denoted by <code class="docutils literal notranslate"><span class="pre">A</span> <span class="pre">&#8594;&#8336;[R]</span> <span class="pre">B</span></code>.</p>
<p>Important examples of non-commutative algebras include algebras of endomorphisms and
algebras of square matrices, both of which will be covered in the chapter on linear algebra.
In this chapter we will discuss one of the most important examples of a commutative algebra,
namely, polynomial algebras.</p>
<p>The algebra of univariate polynomials with coefficients in <code class="docutils literal notranslate"><span class="pre">R</span></code> is called <code class="docutils literal notranslate"><span class="pre">Polynomial</span> <span class="pre">R</span></code>,
which can be written as <code class="docutils literal notranslate"><span class="pre">R[X]</span></code> as soon as one opens the <code class="docutils literal notranslate"><span class="pre">Polynomial</span></code> namespace.
The algebra structure map from <code class="docutils literal notranslate"><span class="pre">R</span></code> to <code class="docutils literal notranslate"><span class="pre">R[X]</span></code> is denoted by <code class="docutils literal notranslate"><span class="pre">C</span></code>,
which stands for &#8220;constant&#8221; since the corresponding
polynomial functions are always constant. The indeterminate is denoted by <code class="docutils literal notranslate"><span class="pre">X</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Polynomial</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">X</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span>
</pre></div>
</div>
<p>In the first example above, it is crucial that we give Lean the expected type since it cannot be
determined from the body of the definition. In the second example, the target polynomial
algebra can be inferred from our use of <code class="docutils literal notranslate"><span class="pre">C</span> <span class="pre">r</span></code> since the type of <code class="docutils literal notranslate"><span class="pre">r</span></code> is known.</p>
<p>Because <code class="docutils literal notranslate"><span class="pre">C</span></code> is a ring morphism from <code class="docutils literal notranslate"><span class="pre">R</span></code> to <code class="docutils literal notranslate"><span class="pre">R[X]</span></code>, we can use all ring morphisms lemmas
such as <code class="docutils literal notranslate"><span class="pre">map_zero</span></code>, <code class="docutils literal notranslate"><span class="pre">map_one</span></code>, <code class="docutils literal notranslate"><span class="pre">map_mul</span></code>, and <code class="docutils literal notranslate"><span class="pre">map_pow</span></code> before computing in the ring
<code class="docutils literal notranslate"><span class="pre">R[X]</span></code>. For example:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">C.map_pow</span><span class="o">]</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>You can access coefficients using <code class="docutils literal notranslate"><span class="pre">Polynomial.coeff</span></code></p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="o">:</span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="bp">.</span><span class="n">coeff</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="bp">.</span><span class="n">coeff</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Defining the degree of a polynomial is always tricky because of the special case of the zero
polynomial. Mathlib has two variants: <code class="docutils literal notranslate"><span class="pre">Polynomial.natDegree</span> <span class="pre">:</span> <span class="pre">R[X]</span> <span class="pre">&#8594;</span> <span class="pre">&#8469;</span></code> assigns degree
<code class="docutils literal notranslate"><span class="pre">0</span></code> to the zero polynomial, and <code class="docutils literal notranslate"><span class="pre">Polynomial.degree</span> <span class="pre">:</span> <span class="pre">R[X]</span> <span class="pre">&#8594;</span> <span class="pre">WithBot</span> <span class="pre">&#8469;</span></code> assigns <code class="docutils literal notranslate"><span class="pre">&#8869;</span></code>.
In the latter, <code class="docutils literal notranslate"><span class="pre">WithBot</span> <span class="pre">&#8469;</span></code> can be seen as <code class="docutils literal notranslate"><span class="pre">&#8469;</span> <span class="pre">&#8746;</span> <span class="pre">{-&#8734;}</span></code>, except that <code class="docutils literal notranslate"><span class="pre">-&#8734;</span></code> is denoted <code class="docutils literal notranslate"><span class="pre">&#8869;</span></code>,
the same symbol as the bottom element in a complete lattice. This special value is used as the
degree of the zero polynomial, and it is absorbent for addition. (It is almost absorbent for
multiplication, except that <code class="docutils literal notranslate"><span class="pre">&#8869;</span> <span class="pre">*</span> <span class="pre">0</span> <span class="pre">=</span> <span class="pre">0</span></code>.)</p>
<p>Morally speaking, the <code class="docutils literal notranslate"><span class="pre">degree</span></code> version is the correct one. For instance, it allows us to state
the expected formula for the degree of a product (assuming the base ring has no zero divisor).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Semiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NoZeroDivisors</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">degree</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">degree</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">degree</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Polynomial.degree_mul</span>
</pre></div>
</div>
<p>Whereas the version for <code class="docutils literal notranslate"><span class="pre">natDegree</span></code> needs to assume non-zero polynomials.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Semiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NoZeroDivisors</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]}</span><span class="w"> </span><span class="o">(</span><span class="n">hp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">natDegree</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Polynomial.natDegree_mul</span><span class="w"> </span><span class="n">hp</span><span class="w"> </span><span class="n">hq</span>
</pre></div>
</div>
<p>However, <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> is much nicer to use than <code class="docutils literal notranslate"><span class="pre">WithBot</span> <span class="pre">&#8469;</span></code>, so Mathlib makes both versions available
and provides lemmas to convert between them. Also, <code class="docutils literal notranslate"><span class="pre">natDegree</span></code> is the more convenient definition
to use when computing the degree of a composition. Composition of polynomial is <code class="docutils literal notranslate"><span class="pre">Polynomial.comp</span></code>
and we have:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Semiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NoZeroDivisors</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">natDegree</span><span class="w"> </span><span class="o">(</span><span class="n">comp</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Polynomial.natDegree_comp</span>
</pre></div>
</div>
<p>Polynomials give rise to polynomial functions: any polynomial can be evaluated on <code class="docutils literal notranslate"><span class="pre">R</span></code>
using <code class="docutils literal notranslate"><span class="pre">Polynomial.eval</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">P.eval</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="bp">.</span><span class="n">eval</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>In particular, there is a predicate, <code class="docutils literal notranslate"><span class="pre">IsRoot</span></code>, that holds for elements <code class="docutils literal notranslate"><span class="pre">r</span></code> in <code class="docutils literal notranslate"><span class="pre">R</span></code> where a
polynomial vanishes.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsRoot</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">P.eval</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>We would like to say that, assuming <code class="docutils literal notranslate"><span class="pre">R</span></code> has no zero divisor, a polynomial has at most as many
roots as its degree, where the roots are counted with multiplicities.
But once again the case of the zero polynomial is painful.
So Mathlib defines <code class="docutils literal notranslate"><span class="pre">Polynomial.roots</span></code> to send a polynomial <code class="docutils literal notranslate"><span class="pre">P</span></code> to a multiset,
i.e. the finite set that is defined to be empty if <code class="docutils literal notranslate"><span class="pre">P</span></code> is zero and the roots of <code class="docutils literal notranslate"><span class="pre">P</span></code>,
with multiplicities, otherwise. This is defined only when the underlying ring is a domain
since otherwise the definition does not have good properties.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsDomain</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="bp">.</span><span class="n">roots</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">r</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">roots_X_sub_C</span><span class="w"> </span><span class="n">r</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsDomain</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">):</span>
<span class="w">    </span><span class="o">((</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">roots</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">{</span><span class="n">r</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Both <code class="docutils literal notranslate"><span class="pre">Polynomial.eval</span></code> and <code class="docutils literal notranslate"><span class="pre">Polynomial.roots</span></code> consider only the coefficients ring. They do not
allow us to say that <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">-</span> <span class="pre">2</span> <span class="pre">:</span> <span class="pre">&#8474;[X]</span></code> has a root in <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> or that <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">+</span> <span class="pre">1</span> <span class="pre">:</span> <span class="pre">&#8477;[X]</span></code> has a root in
<code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>. For this, we need <code class="docutils literal notranslate"><span class="pre">Polynomial.aeval</span></code>, which will evaluate <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">:</span> <span class="pre">R[X]</span></code> in any <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebra.
More precisely, given a semiring <code class="docutils literal notranslate"><span class="pre">A</span></code> and an instance of <code class="docutils literal notranslate"><span class="pre">Algebra</span> <span class="pre">R</span> <span class="pre">A</span></code>, <code class="docutils literal notranslate"><span class="pre">Polynomial.aeval</span></code> sends
every element of <code class="docutils literal notranslate"><span class="pre">a</span></code> along the <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebra morphism of evaluation at <code class="docutils literal notranslate"><span class="pre">a</span></code>. Since <code class="docutils literal notranslate"><span class="pre">AlgHom</span></code>
has a coercion to functions, one can apply it to a polynomial.
But <code class="docutils literal notranslate"><span class="pre">aeval</span></code> does not have a polynomial as an argument, so one cannot use dot notation like in
<code class="docutils literal notranslate"><span class="pre">P.eval</span></code> above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">aeval</span><span class="w"> </span><span class="n">Complex.I</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>The function corresponding to <code class="docutils literal notranslate"><span class="pre">roots</span></code> in this context is <code class="docutils literal notranslate"><span class="pre">aroots</span></code> which takes a polynomial
and then an algebra and outputs a multiset (with the same caveat about the zero polynomial as
for <code class="docutils literal notranslate"><span class="pre">roots</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Complex</span><span class="w"> </span><span class="n">Polynomial</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">aroots</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">Complex.I</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">I</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">suffices</span><span class="w"> </span><span class="n">roots</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">I</span><span class="o">}</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span><span class="w"> </span><span class="o">[</span><span class="n">aroots_def</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">factored</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">I</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="k">have</span><span class="w"> </span><span class="n">key</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">C_mul</span><span class="o">]</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">C_neg</span><span class="o">]</span>
<span class="w">    </span><span class="n">linear_combination</span><span class="w"> </span><span class="n">key</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">p_ne_zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">I</span><span class="o">))</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">H</span>
<span class="w">    </span><span class="n">apply_fun</span><span class="w"> </span><span class="n">eval</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">H</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">eval</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">H</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">factored</span><span class="o">,</span><span class="w"> </span><span class="n">roots_mul</span><span class="w"> </span><span class="n">p_ne_zero</span><span class="o">,</span><span class="w"> </span><span class="n">roots_X_sub_C</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="c1">-- Mathlib knows about D&#39;Alembert-Gauss theorem: ``&#8450;`` is algebraically closed.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsAlgClosed</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>More generally, given an ring morphism <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">R</span> <span class="pre">&#8594;+*</span> <span class="pre">S</span></code> one can evaluate <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">:</span> <span class="pre">R[X]</span></code> at a point
in <code class="docutils literal notranslate"><span class="pre">S</span></code> using <code class="docutils literal notranslate"><span class="pre">Polynomial.eval&#8322;</span></code>. This one produces an actual function from <code class="docutils literal notranslate"><span class="pre">R[X]</span></code> to <code class="docutils literal notranslate"><span class="pre">S</span></code>
since it does not assume the existence of a <code class="docutils literal notranslate"><span class="pre">Algebra</span> <span class="pre">R</span> <span class="pre">S</span></code> instance, so dot notation works as
you would expect.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Complex.ofRealHom</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="bp">.</span><span class="n">eval&#8322;</span><span class="w"> </span><span class="n">Complex.ofRealHom</span><span class="w"> </span><span class="n">Complex.I</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Let us end by mentioning multivariate polynomials briefly. Given a commutative semiring <code class="docutils literal notranslate"><span class="pre">R</span></code>,
the <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebra of polynomials with coefficients in <code class="docutils literal notranslate"><span class="pre">R</span></code> and indeterminates indexed by
a type <code class="docutils literal notranslate"><span class="pre">&#963;</span></code> is <code class="docutils literal notranslate"><span class="pre">MVPolynomial</span> <span class="pre">&#963;</span> <span class="pre">R</span></code>. Given <code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#963;</span></code>, the corresponding polynomial is
<code class="docutils literal notranslate"><span class="pre">MvPolynomial.X</span> <span class="pre">i</span></code>. (As usual, one can open the <code class="docutils literal notranslate"><span class="pre">MVPolynomial</span></code> namespace to shorten this
to <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">i</span></code>.)
For instance, if we want two indeterminates we can use
<code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">2</span></code> as <code class="docutils literal notranslate"><span class="pre">&#963;</span></code> and write the polynomial defining the unit circle in <span class="math notranslate nohighlight">\(\mathbb{R}^2`\)</span> as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">MvPolynomial</span>

<span class="kd">def</span><span class="w"> </span><span class="n">circleEquation</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MvPolynomial</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">1</span>
</pre></div>
</div>
<p>Recall that function application has a very high precedence so the expression above is read as
<code class="docutils literal notranslate"><span class="pre">(X</span> <span class="pre">0)</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">+</span> <span class="pre">(X</span> <span class="pre">1)</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">-</span> <span class="pre">1</span></code>.
We can evaluate it to make sure the point with coordinates <span class="math notranslate nohighlight">\((1, 0)\)</span> is on the circle.
Recall the <code class="docutils literal notranslate"><span class="pre">![...]</span></code> notation denotes elements of <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">X</span></code> for some natural number <code class="docutils literal notranslate"><span class="pre">n</span></code>
determined by the number of arguments and some type <code class="docutils literal notranslate"><span class="pre">X</span></code> determined by the type of arguments.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MvPolynomial.eval</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="o">]</span><span class="w"> </span><span class="n">circleEquation</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">circleEquation</span><span class="o">]</span>
</pre></div>
</div>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C08_Hierarchies.html" class="btn btn-neutral float-left" title="8. Hierarchies" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C10_Linear_Algebra.html" class="btn btn-neutral float-right" title="10. Linear algebra" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>